{
 "metadata": {
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  },
  "orig_nbformat": 2,
  "kernelspec": {
   "name": "python3",
   "display_name": "Python 3.7.3 64-bit ('ml2': pyenv)"
  },
  "interpreter": {
   "hash": "8caa4319d59a734f94e739df6b594acde678ec5f2e3eb7152d087fc4a1992669"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2,
 "cells": [
  {
   "cell_type": "markdown",
   "source": [
    "# Linear-time Temporal Logic (LTL)"
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## LTL Lexer"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "source": [
    "from ml2.ltl import lex_ltl"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "source": [
    "lex_ltl('a U X b')"
   ],
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "['a', 'U', 'X', 'b']"
      ]
     },
     "metadata": {},
     "execution_count": 2
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## LTL Parser"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "source": [
    "from ml2.ltl import parse_ltl"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "source": [
    "parse_ltl('X a R b')"
   ],
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "BinaryAST('R', [BinaryAST('X', [BinaryAST('a', [])]), BinaryAST('b', [])])"
      ]
     },
     "metadata": {},
     "execution_count": 4
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## LTL Formula"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "source": [
    "from ml2.ltl import LTLFormula"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "source": [
    "formula = LTLFormula.from_str('a U G b', 'infix')"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "source": [
    "formula.ast"
   ],
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "BinaryAST('U', [BinaryAST('a', []), BinaryAST('G', [BinaryAST('b', [])])])"
      ]
     },
     "metadata": {},
     "execution_count": 7
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## LTL Spec"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "source": [
    "from ml2.ltl import LTLSpec"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "source": [
    "spec_dict = {\n",
    "    \"assumptions\": [\n",
    "      \"G i0\",\n",
    "      \"i0 & i1\"\n",
    "    ],\n",
    "    \"guarantees\": [\n",
    "        \"G ! (o0 & o1)\",\n",
    "        \"(G ((i0) -> (F (o0))))\",\n",
    "        \"(G ((i1) -> (F (o1))))\"\n",
    "      ],\n",
    "      \"inputs\": [\n",
    "        \"i0\",\n",
    "        \"i1\"\n",
    "      ],\n",
    "      \"outputs\": [\n",
    "        \"o0\",\n",
    "        \"o1\"\n",
    "      ],\n",
    "}"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "source": [
    "spec = LTLSpec.from_dict(spec_dict)"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## LTL Spec Encoder"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "source": [
    "from ml2.ltl import LTLSpecPropertyEncoder\n",
    "from ml2.data.expr import ExprNotation\n",
    "from ml2.data.ast import TPEFormat\n",
    "from ml2.data import vocabulary"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "source": [
    "vocab = vocabulary.from_iterable(['<p>', 'i0', 'i1', 'o0', 'o1', 'G', 'F', '&', '!', '->', '<s>'])"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "INFO:root:Constructed vocabulary containing 11 tokens\n"
     ]
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "source": [
    "encoder = LTLSpecPropertyEncoder(property_pad=10, num_properties=7, notation=ExprNotation.INFIX, encoded_notation=ExprNotation.PREFIX, eos=False, tpe_format=TPEFormat.BRANCHDOWN, tpe_pad=8, vocabulary=vocab)"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "source": [
    "encoder.encode(spec)"
   ],
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "execution_count": 14
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "source": [
    "encoder.tensor"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "2021-07-30 15:11:33.967686: I tensorflow/core/platform/cpu_feature_guard.cc:142] This TensorFlow binary is optimized with oneAPI Deep Neural Network Library (oneDNN) to use the following CPU instructions in performance-critical operations:  AVX2 FMA\n",
      "To enable them in other operations, rebuild TensorFlow with the appropriate compiler flags.\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "(<tf.Tensor: shape=(7, 10), dtype=int32, numpy=\n",
       " array([[10,  5,  1,  0,  0,  0,  0,  0,  0,  0],\n",
       "        [10,  7,  1,  2,  0,  0,  0,  0,  0,  0],\n",
       "        [ 5,  8,  7,  3,  4,  0,  0,  0,  0,  0],\n",
       "        [ 5,  9,  1,  6,  3,  0,  0,  0,  0,  0],\n",
       "        [ 5,  9,  2,  6,  4,  0,  0,  0,  0,  0],\n",
       "        [ 0,  0,  0,  0,  0,  0,  0,  0,  0,  0],\n",
       "        [ 0,  0,  0,  0,  0,  0,  0,  0,  0,  0]], dtype=int32)>,\n",
       " <tf.Tensor: shape=(7, 10, 8), dtype=int32, numpy=\n",
       " array([[[0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0]],\n",
       " \n",
       "        [[0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 1, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0]],\n",
       " \n",
       "        [[0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 1, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 1, 0, 1, 0, 0, 0],\n",
       "         [1, 0, 1, 0, 0, 1, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0]],\n",
       " \n",
       "        [[0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 1, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 1, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 1, 1, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0]],\n",
       " \n",
       "        [[0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 1, 0, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 1, 0, 0, 0, 0],\n",
       "         [1, 0, 0, 1, 1, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0]],\n",
       " \n",
       "        [[0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0]],\n",
       " \n",
       "        [[0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0],\n",
       "         [0, 0, 0, 0, 0, 0, 0, 0]]], dtype=int32)>)"
      ]
     },
     "metadata": {},
     "execution_count": 15
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "source": [
    "encoder.error"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## LTL Spec Data"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "source": [
    "import os\n",
    "from ml2.ltl import LTLSpecData"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "source": [
    "data = LTLSpecData.load('sc-0')"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "INFO:ml2.artifact:Found data sc-0 locally\n",
      "INFO:ml2.ltl.ltl_spec.ltl_spec_data:Successfully constructed dataset of 346 LTL specifications\n"
     ]
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "source": [
    "data.stats()"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "Computed statistics of 346 specifications\n",
      "Number of inputs\n",
      "minimum: 0 maximum: 25 mean: 4.942196531791907 median: 4.0 total: 1710\n",
      "Number of outputs\n",
      "minimum: 1 maximum: 37 mean: 3.979768786127168 median: 2.0 total: 1377\n",
      "Number of assumptions\n",
      "minimum: 0 maximum: 13 mean: 0.5780346820809249 median: 0.0 total: 200\n",
      "Number of guarantees\n",
      "minimum: 1 maximum: 49 mean: 6.658959537572255 median: 4.0 total: 2304\n"
     ]
    }
   ],
   "metadata": {}
  }
 ]
}